package nl.cwi.arne.generator.mcrl2;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;

import nl.cwi.arne.Network;
import nl.cwi.arne.NetworkActivation;
import nl.cwi.arne.Node;
import nl.cwi.arne.NodeActivation;
import nl.cwi.arne.mcrl2.Action;
import nl.cwi.arne.mcrl2.Atom;
import nl.cwi.arne.mcrl2.AtomicAction;
import nl.cwi.arne.mcrl2.BasicTerm;
import nl.cwi.arne.mcrl2.Choice;
import nl.cwi.arne.mcrl2.Comparator;
import nl.cwi.arne.mcrl2.Comparison;
import nl.cwi.arne.mcrl2.Conjunction;
import nl.cwi.arne.mcrl2.Constraint;
import nl.cwi.arne.mcrl2.Element;
import nl.cwi.arne.mcrl2.Function;
import nl.cwi.arne.mcrl2.FunctionCall;
import nl.cwi.arne.mcrl2.Implication;
import nl.cwi.arne.mcrl2.Instance;
import nl.cwi.arne.mcrl2.PrimitiveType;
import nl.cwi.arne.mcrl2.Process;
import nl.cwi.arne.mcrl2.Sequence;
import nl.cwi.arne.mcrl2.SortType;
import nl.cwi.arne.mcrl2.Specification;
import nl.cwi.arne.mcrl2.Structure;
import nl.cwi.arne.mcrl2.Summation;
import nl.cwi.arne.mcrl2.Term;
import nl.cwi.arne.mcrl2.TupleType;
import nl.cwi.arne.mcrl2.Type;

import org.eclipse.emf.ecore.util.EcoreUtil;

/**
 * Arne mCRL2 translator.
 * @author Christian Krause
 */
public class ArneMCRL2Translator {

	public static final Type LEVEL_TYPE = PrimitiveType.INT;
	public static final Type DELTA_TYPE = PrimitiveType.INT;

	// The network:
	private Network network;
	
	// Generated mCRL2 specification:
	private Specification specification;
	
	// The network process:
	private Process process;
	
	// Sort for the nodes:
	private Structure nodesSort;
	
	// Atoms for slow and fast level changes:
	private Atom slow, fast;

	// Whether to show zero changes:
	private boolean withZeroChanges = false;

	// Whether to always start from zero change:
	private boolean startFromZeroChange = false;
	
	// Whether to use deltas for the transition labels.
	private boolean deltaLabels;
	
	// Whether to use verbose labels.
	private boolean verboseLabels;
	
	/**
	 * Generate an mCRL2 specification from a network.
	 * @param network Network.
	 */
	public Specification generateSpecification(NetworkActivation activation) {
		
		// Create a specification.
		network = activation.getNetwork();
		specification = new Specification();
		
		// Create node sort.
		if (!verboseLabels) {
			nodesSort = createNodesSort();
			specification.getSorts().add(nodesSort);
		}
		
		// Create the data type for the actions:
		Type actionType = createActionType();
		
		// Create the "set" or "slow" atom.
		String label = deltaLabels ? "change" : "set";
		slow = new Atom(label, actionType);
		if (network.hasDifferentialEdges()) {
			slow.setName(slow.getName() + "_slow");
		}
		specification.getAtoms().add(slow);
		
		// Create the "fast" atom if required:
		if (network.hasDifferentialEdges()) {
			fast = new Atom(label+"_fast", actionType);
			specification.getAtoms().add(fast);			
		}
		
		// Create the step function:
		Function step = ArneMCRL2FunctionFactory.createStepFunction(specification);
		
		// Create the activation functions:
		Map<Node,Function> activationFunctions = new HashMap<Node,Function>();
		for (Node node : network.getNodes()) {
			if (!node.getIncoming().isEmpty()) {
				NodeActivation current = activation.getNodeActivation(node);
				Function act = ArneMCRL2FunctionFactory.createActivationFunction(current, specification);
				activationFunctions.put(node, act);
			}
		}
		
		// Create the change functions:
		List<Function> changeFunctions = new ArrayList<Function>();
		for (Node node : network.getNodes()) {
			Function act = activationFunctions.get(node);
			Function chg = ArneMCRL2FunctionFactory.createChangeFunction(node, act, step, specification);
			changeFunctions.add(chg);
		}
		
		// Now create the network process:
		process = new Process("network");
		NetworkArguments args = newArgs(process.getArguments());
		
		// Asynchronous semantics: create the main choice:
		Choice choice = new Choice();
		for (int index=0; index<network.getNodes().size(); index++) {
			Node node = network.getNodes().get(index);
			Function change = changeFunctions.get(index);
			choice.getActions().add(createNodeAction(node, change, args));
		}
		process.setAction(choice);
		
		specification.getProcesses().add(process);
		specification.setInitial(createInitialAction());
		return specification;
		
	}
	
	/*
	 * Create the initial network action.
	 */
	private Action createInitialAction() {
		
		// Create a summation with arguments.
		Summation summation = new Summation();
		NetworkArguments args = newArgs(summation.getArguments());
		
		// Remove deltas from the summation again, if we start from zero change:
		if (startFromZeroChange) {
			while (summation.getArguments().size()>network.getNodes().size()) {
				summation.getArguments().remove(network.getNodes().size());
			}			
		}		
		// Also remove the variables where we now the start level:
		for (int i=network.getNodes().size()-1; i>=0; i--) {
			if (network.getNodes().get(i).getStartLevel()>=0) {
				summation.getArguments().remove(i);
			}
		}
		
		// Create a new process instance:
		Instance instance = new Instance(process);
		for (int i=0; i<network.getNodes().size(); i++) {
			byte startLevel = network.getNodes().get(i).getStartLevel();
			instance.getArguments().add(startLevel>=0 ? new BasicTerm(startLevel) : new BasicTerm(args.level(i)));
		}
		for (int i=0; i<network.getNodes().size(); i++) {
			instance.getArguments().add(startFromZeroChange ? new BasicTerm(0) : new BasicTerm(args.delta(i)));
		}
		
		// Use a constraint to restrict the possible values:
		Conjunction conjunction = new Conjunction();
		List<Constraint> constraints = conjunction.getChildren();
		for (int i=0; i<network.getNodes().size(); i++) {
			Node node = network.getNodes().get(i);
			if (node.getStartLevel()<0) {
				constraints.add(new Comparison(new BasicTerm(args.level(i)), Comparator.GREATER_EQUAL, new BasicTerm(0)));
				constraints.add(new Comparison(new BasicTerm(args.level(i)), Comparator.LESS, new BasicTerm(node.getLevels())));
			}
			if (!startFromZeroChange) {
				constraints.add(new Comparison(new BasicTerm(args.delta(i)), Comparator.GREATER_EQUAL, new BasicTerm(-1)));
				constraints.add(new Comparison(new BasicTerm(args.delta(i)), Comparator.LESS_EQUAL, new BasicTerm(1)));
			}
		}
		summation.setAction(new Implication(conjunction, instance));
		return summation;
		
	}
	
	/*
	 * Create a node action.
	 */
	private Action createNodeAction(Node node, Function changeFunction, NetworkArguments args) {
		
		FunctionCall newDelta = new FunctionCall(changeFunction);
		args.makeTerms(newDelta.getArguments());

		Term updatedLevel = new BasicTerm(args.level(node).getName() + "+" + copy(newDelta), LEVEL_TYPE);
		Term updatedDelta = new BasicTerm(args.delta(node).getName() + "+" + copy(newDelta), DELTA_TYPE);
		
		Instance fastInstance = new Instance(process);
		Instance slowInstance = new Instance(process);

		// Updated levels:
		for (Node other : network.getNodes()) {
			if (node==other) {
				fastInstance.getArguments().add(copy(updatedLevel)); // Update the current level
				slowInstance.getArguments().add(copy(updatedLevel));
			} else {
				fastInstance.getArguments().add(new BasicTerm(args.level(other))); // No level change
				slowInstance.getArguments().add(new BasicTerm(args.level(other)));
			}
		}
		
		// Updated deltas:
		for (Node other : network.getNodes()) {
			if (node==other) {
				fastInstance.getArguments().add(copy(updatedDelta));	// Update the old delta
				slowInstance.getArguments().add(copy(newDelta));		// Use the new delta
			} else {
				fastInstance.getArguments().add(new BasicTerm(args.delta(other)));		// No delta change
				slowInstance.getArguments().add(new BasicTerm(0));						// Reset the delta
			}
		}

		AtomicAction fastAtom = new AtomicAction(fast);
		AtomicAction slowAtom = new AtomicAction(slow);
		
		if (verboseLabels) {
			int nodes = network.getNodes().size();
			int start = deltaLabels ? nodes / 2 : 0;
			for (int i=start; i<start+nodes; i++) {
				slowAtom.getArguments().add(copy(slowInstance.getArguments().get(i)));
				fastAtom.getArguments().add(copy(fastInstance.getArguments().get(i)));
			}
		} else {
			slowAtom.getArguments().add(new BasicTerm(getNodeElem(node)));
			fastAtom.getArguments().add(new BasicTerm(getNodeElem(node)));
			slowAtom.getArguments().add(copy(deltaLabels ? updatedDelta : updatedLevel));
			fastAtom.getArguments().add(copy(deltaLabels ? updatedDelta : updatedLevel));			
		}
		
		// Create a sequence of the main action and the new instance:
		Action fastAction = new Sequence(fastAtom, fastInstance);
		Action slowAction = new Sequence(slowAtom, slowInstance);
		
		// The main action is based on the fast-check:
		Action main = new Implication(ArneMCRL2ConstraintFactory.createFastCheck(node, args), fastAction, slowAction);

		// Constraint to make sure the change is not zero (avoid self loops in the LTS):
		Constraint zeroCheck = new Comparison(copy(newDelta), Comparator.NOT_EQUAL, new BasicTerm(0));

		// Wrap the action in an implication: 
		Action result = new Implication(zeroCheck, main);

		// Add self loops again if required:
		if (withZeroChanges) {
			
			Instance zeroInstance = new Instance(process);
			
			for (Node other : network.getNodes()) {
				zeroInstance.getArguments().add(new BasicTerm(args.level(other))); // No changes
			}
			for (Node other : network.getNodes()) {
				zeroInstance.getArguments().add(new BasicTerm(args.delta(other))); // No changes
			}

			AtomicAction zeroAtom = new AtomicAction(slow);
			if (verboseLabels) {
				for (Node current : network.getNodes()) {
					Term currentLevel = new BasicTerm(args.level(current).getName(), LEVEL_TYPE);
					Term currentDelta = new BasicTerm(args.delta(current).getName(), DELTA_TYPE);
					zeroAtom.getArguments().add(deltaLabels ? currentDelta : currentLevel);
				}
			} else {
				Term currentLevel = new BasicTerm(args.level(node).getName(), LEVEL_TYPE);
				Term currentDelta = new BasicTerm(args.delta(node).getName(), DELTA_TYPE);
				zeroAtom.getArguments().add(new BasicTerm(getNodeElem(node)));
				zeroAtom.getArguments().add(copy(deltaLabels ? currentDelta : currentLevel));
			}
			
			Action zeroAction = new Sequence(zeroAtom, zeroInstance);			
			result = new Choice(zeroAction, result);
			
		}
		
		return result;
		
	}	
		
	/*
	 * Get the type of actions.
	 */
	private Type createActionType() {
		TupleType type = new TupleType();
		if (verboseLabels) {
			for (int i=0; i<network.getNodes().size(); i++) {
				type.getChildren().add(deltaLabels ? DELTA_TYPE : LEVEL_TYPE);
			}
		} else {
			type.getChildren().add(new SortType(nodesSort));
			type.getChildren().add(deltaLabels ? DELTA_TYPE : LEVEL_TYPE);
		}
		return type;
	}
	
	private Structure createNodesSort() {
		Structure nodesSort = new Structure("Node");
		for (Node node : network.getNodes()) {
			nodesSort.getElements().add(new Element(node.getName()));
		}
		return nodesSort;
	}
	
	private NetworkArguments newArgs(List<Atom> container) {
		return new NetworkArguments(network, container, LEVEL_TYPE, DELTA_TYPE);
	}
	
	private Term copy(Term term) {
		return EcoreUtil.copy(term);
	}
	
	public Process getNetworkProcess() {
		return process;
	}
	
	private Element getNodeElem(Node node) {
		return nodesSort.getElements().get(network.getNodes().indexOf(node));
	}

	public void setWithZeroChanges(boolean withZeroChanges) {
		this.withZeroChanges = withZeroChanges;
	}

	public void setStartFromZeroChange(boolean startFromZeroChange) {
		this.startFromZeroChange = startFromZeroChange;
	}
	
	public void setDeltaLabels(boolean deltaLabels) {
		this.deltaLabels = deltaLabels;
	}
	
	public void setVerboseLabels(boolean verboseLabels) {
		this.verboseLabels = verboseLabels;
	}
}
